Inference at * 1 
Iof proof for Lemma equal-bnot:



1. x : 
2. y : 
3. (y)
4. x
  (x) 

latex

 by (D 0) 
CollapseTHEN (Auto) 

latex

C.

Definitions

x:AB(x), b, A, P  Q, False